es:ES, ds:x:Id fp Type, e:E.
@loc(e) discrete ds  ((first(e)))  (state after pred(e) = (state when e)  State(ds)) 

latex

Definitions

ff, tt, if b then t else f fi , Top, f(x)?z, , P & Q, P  Q, P  Q, x. t(x), t  T, P  Q, x:A. B(x), Unit, , @i(x:T), xdom(f). v=f(x)   P(x;v), @i discrete ds, {T}, SQType(T), x(s),

Lemmas

es-dstate-subtype, decl-state wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf, es-vartype wf, bnot wf, bool wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, es-state-subtype, es-state-when wf, dstate-after-pred, es-dstate-when wf, es-state-after-dstate-after, es-state-when-dstate-when, es-state-dstate-subtype, es-state-after wf, Id sq, es-loc-pred, event system wf, Id wf, fpf wf, es-E wf, es-loc wf, es-dds wf, es-first wf, assert wf, not wf